package ss.pku.jsa.type.inference;

import java.io.FileInputStream;
import java.util.Iterator;

import ss.pku.jsa.type.constraint.solver.Native;
import ss.pku.jsa.type.constraint.solver.QError;


@SuppressWarnings({ "rawtypes" })
public class CQual {
	// private static void makeEq(Qualifier left, Qualifier right, QualGate
	// qgate, Location loc, int polarity, QError error)
	// {
	// makeEdge(Constraint.Kind.LT, left, right, qgate, loc, polarity, error);
	// makeEdge(Constraint.Kind.LT, right, left, qgate, loc, polarity, error);
	// }

	public static void makeEdge(Constraint.Kind kind, Qualifier left,
			Qualifier right, QualGate qgate, Location loc, int polarity,
			QError error) {
		if ((left == null) || (right == null)) {
			return;
		}

		if ((JqualPlugin.noGates) || (qgate == null)) {
			qgate = QualGate.EMPTY;
		}

		if (polarity == 0) {
			if (qgate == QualGate.EMPTY) {
				if (JqualPlugin.logConstraints) {
					JqualPlugin.printlnLog("constraintLog", left + " <= "
							+ right + " " + loc + " " + error);
				}

				if (kind == Constraint.Kind.LT)
					Native.mkleqQual(loc.getNativeIndex(),
							left.getNativeIndex(), right.getNativeIndex(),
							error.num);
				else
					Native.mkeqQual(loc.getNativeIndex(),
							left.getNativeIndex(), right.getNativeIndex(),
							error.num);
			} else {
				if (JqualPlugin.logConstraints) {
					JqualPlugin.printlnLog("constraintLog", left + " <="
							+ qgate + " " + right + " " + loc + " " + error);
				}

				if (kind == Constraint.Kind.LT)
					Native.mkleqQualGated(qgate.getNativeIndex(),
							loc.getNativeIndex(), left.getNativeIndex(),
							right.getNativeIndex(), error.num);
				else
					Native.mkeqQualGated(qgate.getNativeIndex(),
							loc.getNativeIndex(), left.getNativeIndex(),
							right.getNativeIndex(), error.num);
			}
		} else {
			int polIndex = polarity * loc.locIndex;
			if (JqualPlugin.logConstraints) {
				JqualPlugin.printlnLog("constraintLog", left + " <=("
						+ polIndex + ")" + qgate + " " + right + " " + loc
						+ " " + error);
			}
			if (kind == Constraint.Kind.LT) {
				Native.mkleqInst(qgate.getNativeIndex(), loc.getNativeIndex(),
						polarity, left.getNativeIndex(),
						right.getNativeIndex(), error.num);
			} else {
				Native.mkleqInst(qgate.getNativeIndex(), loc.getNativeIndex(),
						polarity, left.getNativeIndex(),
						right.getNativeIndex(), error.num);
				Native.mkleqInst(qgate.getNativeIndex(), loc.getNativeIndex(),
						Constraint.revPol(polarity), right.getNativeIndex(),
						left.getNativeIndex(), error.num);
			}
		}
	}

	public static void makeMethodConstraint(MethodQType left,
			MethodQType right, QualGate qgate, Location loc, int polarity,
			QError error) {
		if ((left == null) || (right == null)) {
			return;
		}

		if ((left.getReturnQType() != null) && (right.getReturnQType() != null)) {
			Constraint.addConstraint(left.getReturnQType().deref(), right
					.getReturnQType().deref(), qgate, loc, polarity, error,
					Constraint.Kind.LT);
		}

		Constraint.addConstraint(right.getThisQType(), left.getThisQType(),
				qgate, loc, polarity, error, Constraint.Kind.LT);

		Iterator itL = left.getParameterQTypes().iterator();
		for (Iterator itR = right.getParameterQTypes().iterator(); itR
				.hasNext();) {
			if (!itL.hasNext())
				throw new IllegalArgumentException(
						"incompatible methods passed to makeLeq");
			QType r = ((RefQType) itR.next()).deref();
			QType l = ((RefQType) itL.next()).deref();
			Constraint.addConstraint(r, l, qgate, loc, polarity, error,
					Constraint.Kind.LT);
		}
	}

	public static void resetCqual(String lattice, String ffiQuals,
			boolean usePolymorphic, boolean useFFISubtypes, boolean inferEnum,
			int firstPtr, int numPtrs) {
		Native.resetLibQual();

		Native.initCQual(lattice, ffiQuals, useFFISubtypes, inferEnum,
				firstPtr, numPtrs);

		Native.setPolyFlag(usePolymorphic);
		QError.registerQErrors();
	}

	public static FileInputStream finish() {
		String outFile = Native.finishCQual();

		if (outFile == null)
			return null;
		try {
			return new FileInputStream(outFile);
		} catch (Exception localException) {
		}
		throw new IllegalArgumentException("Could not find output file: "
				+ outFile);
	}

	public static int makeQVar(String name, Location loc, boolean preferred,
			boolean global) {
		return Native.makeQvar(name, loc.getNativeIndex(), preferred, global);
	}

	public static boolean leqQual(Qualifier q1, Qualifier q2) {
		return Native.leqQual(q1.getNativeIndex(), q2.getNativeIndex());
	}

	public static boolean mayLeqQual(Qualifier q1, Qualifier q2) {
		boolean r = Native.mayLeqQual(q1.getNativeIndex(), q2.getNativeIndex());
		return r;
	}
}
